Deftorel pass by DCupello1 · Pull Request #206 · Wasm-DSL/spectec

DCupello1 · 2025-11-18T17:05:59Z

This pull request is made to introduce the pass "deftorel". This pass does as the name suggests: convert specific function definitions to relations.

Example:

syntax A = 
  | B{nat : nat}(nat : nat)
  | C

def $foo(A : A) : nat
  def $foo{n : n}(B_A(n)) = 10
    -- if (n < 5)
  def $foo{n : n}(B_A(n)) = 5
    -- if n = 10
  def $foo{varA : A}(varA) = 20

to

relation fun_foo_before_fun_foo_case_1: `%`(A)
  rule fun_foo_case_0{n : nat}:
    `%`(B_A(n))
    -- if (n < 5)

relation fun_foo_before_fun_foo_case_2: `%`(A)
  rule fun_foo_case_1{n : nat}:
    `%`(B_A(n))
    -- ~ fun_foo_before_fun_foo_case_1: `%`(B_A(n))
    -- if (n = 10)
  rule fun_foo_case_0{n : nat}:
    `%`(B_A(n))
    -- if (n < 5)

relation fun_foo: `%%`(A, nat)
  rule fun_foo_case_0{n : nat}:
    `%%`(B_A(n), 10)
    -- if (n < 5)
  rule fun_foo_case_1{n : nat}:
    `%%`(B_A(n), 5)
    -- ~ fun_foo_before_fun_foo_case_1: `%`(B_A(n))
    -- if (n = 10)
  rule fun_foo_case_2{varA : A}:
    `%%`(varA, 20)
    -- ~ fun_foo_before_fun_foo_case_2: `%`(varA)

This pass does not ensure the created relations that handle the fallthrough semantics have unique name (yet).

Currently a draft as its not meant to be mergable yet, since more testing should be done to ensure it does the right thing. But for now it should give a way to track what is happening with this pass.

Validates up to Wasm 3.0. Have not tested it in Rocq, but will probably not compile due to name clashes.

Some todos:

Potentially resolve name clashes as I did in Else pass
Make a new pass that simplifies these generated relations (and also the ones generated by otherwise). This might be tricky because for these you would ideally want:

relation fun_foo: `%%`(A, nat)
  rule fun_foo_case_0{n : nat}:
    `%%`(B_A(n), 10)
    -- if (n < 5)
  rule fun_foo_case_1{n : nat}:
    `%%`(B_A(n), 5)
    -- if n >= 5
    -- if n = 10 
  rule fun_foo_case_2{n : nat , varA : A}:
    `%%`(varA, 20)
    -- (varA != B_A(n) \/ n >= 5)
    -- (varA != B_A(n) \/ n != 10)

This would be possible for boolean conditions but not for anything else. Maybe thats fine?

Only possible for functions with Exp params, since parametrised relations don't exist yet. Will modify once thats done.
Want to order well the generated function-rel premises (since order matters if we make them implications).

nomeata · 2025-11-21T08:44:04Z

I’m trying to merge this into the lean4 branch, but trying to update the test-prose and test-splice test output hangs (or maybe just takes longer than I want to wait). Do you also observe that?

DCupello1 · 2025-11-21T10:39:49Z

Just ran the tests locally again to make sure, it all seems fine to me. I haven't changed either of them, so thats very weird.

DCupello1 · 2025-11-21T10:44:04Z

Also, for visibility (I put this in #207 but not here).

After some testing on the rocq output, it seems like some recursive functions turning into relations do not pass as it doesn't pass the strictly positive condition. Lean will likely exhibit a similar error on the function utf8.

nomeata · 2025-11-21T11:05:23Z

Lean will likely exhibit a similar error on the function utf8.

That function definition is in 5.1-binary.values.spectec – would it make sense to first focus on the other parts of the specification (types, validation and execution), and postpone issues related to the binary and text format?

DCupello1 · 2025-11-21T11:12:57Z

Lean will likely exhibit a similar error on the function utf8.

That function definition is in 5.1-binary.values.spectec – would it make sense to first focus on the other parts of the specification (types, validation and execution), and postpone issues related to the binary and text format?

Fair enough, but did some more quick testing and it happens to most recursive functions (subst_typevar and subst_typeuse for example)

nomeata · 2025-11-21T11:28:06Z

Maybe we need to push harder to make them translate as functions.

At least when the premises are on identical patterns like in

def $subst_typevar(tv, eps, eps) = tv
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = tu_1                            -- if tv = tv_1
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = $subst_typevar(tv, tv'*, tu'*)  -- otherwise

and they are all booleans or otherwise, it should be possible to translate that as if-then-else, shouldn’t it?

DCupello1 · 2025-11-21T11:36:25Z

Maybe we need to push harder to make them translate as functions.

At least when the premises are on identical patterns like in
def $subst_typevar(tv, eps, eps) = tv
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = tu_1                            -- if tv = tv_1
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = $subst_typevar(tv, tv'*, tu'*)  -- otherwise
and they are all booleans or otherwise, it should be possible to translate that as if-then-else, shouldn’t it?

Yes, that was one of the things I was thinking of doing as well, for premises that are boolean conditions. I wanted a more general approach first though to see if it worked.

In some functions by the way, you can also transform some of the if premises into let premises (look at growmem for example) and any iterpr with boolean conditions could be List.all

DCupello1 · 2025-12-08T17:06:27Z

With the new changes, the fallthrough premises no longer cause a (big) problem. Wasm 3.0 was compiled in Rocq (with some spec changes for partial funcs).

DCupello1 · 2026-01-21T11:57:25Z

Changed this to only do fallthrough whenever it spots an otherwise premise, instead of all the time. This is in line with what the actual semantics is supposed to be.

Other than maybe fixing names and reordering premises, this should be good to start being reviewed. It is a pretty complicated one to review though.

nomeata · 2026-01-21T12:48:50Z

It is a pretty complicated one to review though.

Yeah, I’m not sure if I can do a meaningful review :-/

DCupello1 · 2026-01-21T13:47:29Z

It is a pretty complicated one to review though.

Yeah, I’m not sure if I can do a meaningful review :-/

Fair enough! I will probably just keep it as a draft until we make use of this pass in the mechanization backends.

Will also try to make it more readable!

…dles otherwise.

…he recursive functions themselves.

…that removes ones that have reference to the return expression.

…ng new traversal method

…s. Fix tests

…xp params) into relations.

DCupello1 changed the title ~~Deftorel pass [WIP]~~ Deftorel pass Nov 19, 2025

DCupello1 mentioned this pull request Nov 19, 2025

Rocq backend #207

Draft

7 tasks

DCupello1 marked this pull request as ready for review January 21, 2026 10:48

DCupello1 marked this pull request as draft January 21, 2026 13:47

DCupello1 added 7 commits February 23, 2026 12:40

Ported deftorel pass

bde9299

Added fallthrough semantics to converted defs, which conveniently han…

1fbb8bf

…dles otherwise.

Remove created relations out of recursive groups if they don't call t…

f2b665f

…he recursive functions themselves.

Added a filter to the prems from the generated fallthrough relations …

b56f3aa

…that removes ones that have reference to the return expression.

Made fallthrough only when otherwise is present. Refactored a bit usi…

6519b36

…ng new traversal method

Removed subtyping matching check

2366296

reordering so generated deftorel relations get implicit sidecondition…

96f7ea3

…s. Fix tests

DCupello1 force-pushed the deftorel-pass branch from 9c4be10 to 96f7ea3 Compare February 23, 2026 13:06

Make recursive functions (at the current moment, only the ones with e…

e5d20ef

…xp params) into relations.

DCupello1 force-pushed the deftorel-pass branch from 661e6e4 to e5d20ef Compare February 26, 2026 12:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Deftorel pass#206

Deftorel pass#206
DCupello1 wants to merge 8 commits intomainfrom
deftorel-pass

DCupello1 commented Nov 18, 2025 •

edited

Loading

Uh oh!

nomeata commented Nov 21, 2025 •

edited

Loading

Uh oh!

DCupello1 commented Nov 21, 2025 •

edited

Loading

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

nomeata commented Nov 21, 2025

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

nomeata commented Nov 21, 2025

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

DCupello1 commented Dec 8, 2025

Uh oh!

DCupello1 commented Jan 21, 2026

Uh oh!

nomeata commented Jan 21, 2026

Uh oh!

DCupello1 commented Jan 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

DCupello1 commented Nov 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Nov 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

DCupello1 commented Nov 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

nomeata commented Nov 21, 2025

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

nomeata commented Nov 21, 2025

Uh oh!

DCupello1 commented Nov 21, 2025

Uh oh!

DCupello1 commented Dec 8, 2025

Uh oh!

DCupello1 commented Jan 21, 2026

Uh oh!

nomeata commented Jan 21, 2026

Uh oh!

DCupello1 commented Jan 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

DCupello1 commented Nov 18, 2025 •

edited

Loading

nomeata commented Nov 21, 2025 •

edited

Loading

DCupello1 commented Nov 21, 2025 •

edited

Loading